Left Termination of the query pattern
cnfequiv(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 289 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 479 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 36 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 PiDPToQDPProof (⇒, 0 ms)
        ↳16 QDP
        ↳17 QDPOrderProof (⇔, 1181 ms)
        ↳18 QDP
        ↳19 DependencyGraphProof (⇔, 0 ms)
        ↳20 TRUE
    ↳21 PiDP
        ↳22 PiDPToQDPProof (⇒, 12 ms)
        ↳23 QDP
        ↳24 QDPOrderProof (⇔, 943 ms)
        ↳25 QDP
        ↳26 PisEmptyProof (⇔, 0 ms)
        ↳27 YES
    ↳28 PiDP
        ↳29 PiDPToQDPProof (⇒, 0 ms)
        ↳30 QDP
        ↳31 QDPOrderProof (⇔, 83 ms)
        ↳32 QDP
        ↳33 QDPOrderProof (⇔, 912 ms)
        ↳34 QDP
        ↳35 PisEmptyProof (⇔, 0 ms)
        ↳36 YES

(0) Obligation:

Clauses:

cnfequiv(X, Y) :- ','(transform(X, Z), cnfequiv(Z, Y)).
cnfequiv(X, X).
transform(n(n(X)), X).
transform(n(a(X, Y)), o(n(X), n(Y))).
transform(n(o(X, Y)), a(n(X), n(Y))).
transform(o(X, a(Y, Z)), a(o(X, Y), o(X, Z))).
transform(o(a(X, Y), Z), a(o(X, Z), o(Y, Z))).
transform(o(X1, Y), o(X2, Y)) :- transform(X1, X2).
transform(o(X, Y1), o(X, Y2)) :- transform(Y1, Y2).
transform(a(X1, Y), a(X2, Y)) :- transform(X1, X2).
transform(a(X, Y1), a(X, Y2)) :- transform(Y1, Y2).
transform(n(X1), n(X2)) :- transform(X1, X2).

Query: cnfequiv(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

transformB(o(X1, X2), o(X3, X2)) :- transformB(X1, X3).
transformB(o(X1, X2), o(X1, X3)) :- transformB(X2, X3).
transformB(a(X1, X2), a(X3, X2)) :- transformB(X1, X3).
transformB(a(X1, X2), a(X1, X3)) :- transformB(X2, X3).
transformB(n(X1), n(X2)) :- transformB(X1, X2).
cnfequivA(n(n(X1)), X2) :- cnfequivA(X1, X2).
cnfequivA(n(a(X1, X2)), X3) :- cnfequivA(o(n(X1), n(X2)), X3).
cnfequivA(n(o(X1, X2)), X3) :- cnfequivA(a(n(X1), n(X2)), X3).
cnfequivA(o(X1, a(X2, X3)), X4) :- cnfequivA(a(o(X1, X2), o(X1, X3)), X4).
cnfequivA(o(a(X1, X2), X3), X4) :- cnfequivA(a(o(X1, X3), o(X2, X3)), X4).
cnfequivA(o(X1, X2), X3) :- transformB(X1, X4).
cnfequivA(o(X1, X2), X3) :- ','(transformcB(X1, X4), cnfequivA(o(X4, X2), X3)).
cnfequivA(o(X1, X2), X3) :- transformB(X2, X4).
cnfequivA(o(X1, X2), X3) :- ','(transformcB(X2, X4), cnfequivA(o(X1, X4), X3)).
cnfequivA(a(X1, X2), X3) :- transformB(X1, X4).
cnfequivA(a(X1, X2), X3) :- ','(transformcB(X1, X4), cnfequivA(a(X4, X2), X3)).
cnfequivA(a(X1, X2), X3) :- transformB(X2, X4).
cnfequivA(a(X1, X2), X3) :- ','(transformcB(X2, X4), cnfequivA(a(X1, X4), X3)).
cnfequivA(n(X1), X2) :- transformB(X1, X3).
cnfequivA(n(X1), X2) :- ','(transformcB(X1, X3), cnfequivA(n(X3), X2)).

Clauses:

cnfequivcA(n(n(X1)), X2) :- cnfequivcA(X1, X2).
cnfequivcA(n(a(X1, X2)), X3) :- cnfequivcA(o(n(X1), n(X2)), X3).
cnfequivcA(n(o(X1, X2)), X3) :- cnfequivcA(a(n(X1), n(X2)), X3).
cnfequivcA(o(X1, a(X2, X3)), X4) :- cnfequivcA(a(o(X1, X2), o(X1, X3)), X4).
cnfequivcA(o(a(X1, X2), X3), X4) :- cnfequivcA(a(o(X1, X3), o(X2, X3)), X4).
cnfequivcA(o(X1, X2), X3) :- ','(transformcB(X1, X4), cnfequivcA(o(X4, X2), X3)).
cnfequivcA(o(X1, X2), X3) :- ','(transformcB(X2, X4), cnfequivcA(o(X1, X4), X3)).
cnfequivcA(a(X1, X2), X3) :- ','(transformcB(X1, X4), cnfequivcA(a(X4, X2), X3)).
cnfequivcA(a(X1, X2), X3) :- ','(transformcB(X2, X4), cnfequivcA(a(X1, X4), X3)).
cnfequivcA(n(X1), X2) :- ','(transformcB(X1, X3), cnfequivcA(n(X3), X2)).
cnfequivcA(X1, X1).
transformcB(n(n(X1)), X1).
transformcB(n(a(X1, X2)), o(n(X1), n(X2))).
transformcB(n(o(X1, X2)), a(n(X1), n(X2))).
transformcB(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3))).
transformcB(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3))).
transformcB(o(X1, X2), o(X3, X2)) :- transformcB(X1, X3).
transformcB(o(X1, X2), o(X1, X3)) :- transformcB(X2, X3).
transformcB(a(X1, X2), a(X3, X2)) :- transformcB(X1, X3).
transformcB(a(X1, X2), a(X1, X3)) :- transformcB(X2, X3).
transformcB(n(X1), n(X2)) :- transformcB(X1, X2).

Afs:

cnfequivA(x1, x2)  =  cnfequivA(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
cnfequivA_in: (b,f)
transformB_in: (b,f)
transformcB_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(n(n(X1)), X2) → U6_GA(X1, X2, cnfequivA_in_ga(X1, X2))
CNFEQUIVA_IN_GA(n(n(X1)), X2) → CNFEQUIVA_IN_GA(X1, X2)
CNFEQUIVA_IN_GA(n(a(X1, X2)), X3) → U7_GA(X1, X2, X3, cnfequivA_in_ga(o(n(X1), n(X2)), X3))
CNFEQUIVA_IN_GA(n(a(X1, X2)), X3) → CNFEQUIVA_IN_GA(o(n(X1), n(X2)), X3)
CNFEQUIVA_IN_GA(n(o(X1, X2)), X3) → U8_GA(X1, X2, X3, cnfequivA_in_ga(a(n(X1), n(X2)), X3))
CNFEQUIVA_IN_GA(n(o(X1, X2)), X3) → CNFEQUIVA_IN_GA(a(n(X1), n(X2)), X3)
CNFEQUIVA_IN_GA(o(X1, a(X2, X3)), X4) → U9_GA(X1, X2, X3, X4, cnfequivA_in_ga(a(o(X1, X2), o(X1, X3)), X4))
CNFEQUIVA_IN_GA(o(X1, a(X2, X3)), X4) → CNFEQUIVA_IN_GA(a(o(X1, X2), o(X1, X3)), X4)
CNFEQUIVA_IN_GA(o(a(X1, X2), X3), X4) → U10_GA(X1, X2, X3, X4, cnfequivA_in_ga(a(o(X1, X3), o(X2, X3)), X4))
CNFEQUIVA_IN_GA(o(a(X1, X2), X3), X4) → CNFEQUIVA_IN_GA(a(o(X1, X3), o(X2, X3)), X4)
CNFEQUIVA_IN_GA(o(X1, X2), X3) → U11_GA(X1, X2, X3, transformB_in_ga(X1, X4))
CNFEQUIVA_IN_GA(o(X1, X2), X3) → TRANSFORMB_IN_GA(X1, X4)
TRANSFORMB_IN_GA(o(X1, X2), o(X3, X2)) → U1_GA(X1, X2, X3, transformB_in_ga(X1, X3))
TRANSFORMB_IN_GA(o(X1, X2), o(X3, X2)) → TRANSFORMB_IN_GA(X1, X3)
TRANSFORMB_IN_GA(o(X1, X2), o(X1, X3)) → U2_GA(X1, X2, X3, transformB_in_ga(X2, X3))
TRANSFORMB_IN_GA(o(X1, X2), o(X1, X3)) → TRANSFORMB_IN_GA(X2, X3)
TRANSFORMB_IN_GA(a(X1, X2), a(X3, X2)) → U3_GA(X1, X2, X3, transformB_in_ga(X1, X3))
TRANSFORMB_IN_GA(a(X1, X2), a(X3, X2)) → TRANSFORMB_IN_GA(X1, X3)
TRANSFORMB_IN_GA(a(X1, X2), a(X1, X3)) → U4_GA(X1, X2, X3, transformB_in_ga(X2, X3))
TRANSFORMB_IN_GA(a(X1, X2), a(X1, X3)) → TRANSFORMB_IN_GA(X2, X3)
TRANSFORMB_IN_GA(n(X1), n(X2)) → U5_GA(X1, X2, transformB_in_ga(X1, X2))
TRANSFORMB_IN_GA(n(X1), n(X2)) → TRANSFORMB_IN_GA(X1, X2)
CNFEQUIVA_IN_GA(o(X1, X2), X3) → U12_GA(X1, X2, X3, transformcB_in_ga(X1, X4))
U12_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → U13_GA(X1, X2, X3, cnfequivA_in_ga(o(X4, X2), X3))
U12_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(o(X4, X2), X3)
CNFEQUIVA_IN_GA(o(X1, X2), X3) → U14_GA(X1, X2, X3, transformB_in_ga(X2, X4))
CNFEQUIVA_IN_GA(o(X1, X2), X3) → TRANSFORMB_IN_GA(X2, X4)
CNFEQUIVA_IN_GA(o(X1, X2), X3) → U15_GA(X1, X2, X3, transformcB_in_ga(X2, X4))
U15_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → U16_GA(X1, X2, X3, cnfequivA_in_ga(o(X1, X4), X3))
U15_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(o(X1, X4), X3)
CNFEQUIVA_IN_GA(a(X1, X2), X3) → U17_GA(X1, X2, X3, transformB_in_ga(X1, X4))
CNFEQUIVA_IN_GA(a(X1, X2), X3) → TRANSFORMB_IN_GA(X1, X4)
CNFEQUIVA_IN_GA(a(X1, X2), X3) → U18_GA(X1, X2, X3, transformcB_in_ga(X1, X4))
U18_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → U19_GA(X1, X2, X3, cnfequivA_in_ga(a(X4, X2), X3))
U18_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(a(X4, X2), X3)
CNFEQUIVA_IN_GA(a(X1, X2), X3) → U20_GA(X1, X2, X3, transformB_in_ga(X2, X4))
CNFEQUIVA_IN_GA(a(X1, X2), X3) → TRANSFORMB_IN_GA(X2, X4)
CNFEQUIVA_IN_GA(a(X1, X2), X3) → U21_GA(X1, X2, X3, transformcB_in_ga(X2, X4))
U21_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → U22_GA(X1, X2, X3, cnfequivA_in_ga(a(X1, X4), X3))
U21_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(a(X1, X4), X3)
CNFEQUIVA_IN_GA(n(X1), X2) → U23_GA(X1, X2, transformB_in_ga(X1, X3))
CNFEQUIVA_IN_GA(n(X1), X2) → TRANSFORMB_IN_GA(X1, X3)
CNFEQUIVA_IN_GA(n(X1), X2) → U24_GA(X1, X2, transformcB_in_ga(X1, X3))
U24_GA(X1, X2, transformcB_out_ga(X1, X3)) → U25_GA(X1, X2, cnfequivA_in_ga(n(X3), X2))
U24_GA(X1, X2, transformcB_out_ga(X1, X3)) → CNFEQUIVA_IN_GA(n(X3), X2)

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1)), X1) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2)), o(n(X1), n(X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2)), a(n(X1), n(X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3))) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2), o(X3, X2)) → U42_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(o(X1, X2), o(X1, X3)) → U43_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(a(X1, X2), a(X3, X2)) → U44_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(a(X1, X2), a(X1, X3)) → U45_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(n(X1), n(X2)) → U46_ga(X1, X2, transformcB_in_ga(X1, X2))
U46_ga(X1, X2, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The argument filtering Pi contains the following mapping:
cnfequivA_in_ga(x1, x2)  =  cnfequivA_in_ga(x1)
n(x1)  =  n(x1)
a(x1, x2)  =  a(x1, x2)
o(x1, x2)  =  o(x1, x2)
transformB_in_ga(x1, x2)  =  transformB_in_ga(x1)
transformcB_in_ga(x1, x2)  =  transformcB_in_ga(x1)
transformcB_out_ga(x1, x2)  =  transformcB_out_ga(x1, x2)
U42_ga(x1, x2, x3, x4)  =  U42_ga(x1, x2, x4)
U43_ga(x1, x2, x3, x4)  =  U43_ga(x1, x2, x4)
U44_ga(x1, x2, x3, x4)  =  U44_ga(x1, x2, x4)
U45_ga(x1, x2, x3, x4)  =  U45_ga(x1, x2, x4)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
CNFEQUIVA_IN_GA(x1, x2)  =  CNFEQUIVA_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
TRANSFORMB_IN_GA(x1, x2)  =  TRANSFORMB_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x2, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x2, x4)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x2, x4)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x2, x4)
U17_GA(x1, x2, x3, x4)  =  U17_GA(x1, x2, x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x2, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x2, x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x2, x4)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x1, x2, x4)
U22_GA(x1, x2, x3, x4)  =  U22_GA(x1, x2, x4)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U25_GA(x1, x2, x3)  =  U25_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(n(n(X1)), X2) → U6_GA(X1, X2, cnfequivA_in_ga(X1, X2))
CNFEQUIVA_IN_GA(n(n(X1)), X2) → CNFEQUIVA_IN_GA(X1, X2)
CNFEQUIVA_IN_GA(n(a(X1, X2)), X3) → U7_GA(X1, X2, X3, cnfequivA_in_ga(o(n(X1), n(X2)), X3))
CNFEQUIVA_IN_GA(n(a(X1, X2)), X3) → CNFEQUIVA_IN_GA(o(n(X1), n(X2)), X3)
CNFEQUIVA_IN_GA(n(o(X1, X2)), X3) → U8_GA(X1, X2, X3, cnfequivA_in_ga(a(n(X1), n(X2)), X3))
CNFEQUIVA_IN_GA(n(o(X1, X2)), X3) → CNFEQUIVA_IN_GA(a(n(X1), n(X2)), X3)
CNFEQUIVA_IN_GA(o(X1, a(X2, X3)), X4) → U9_GA(X1, X2, X3, X4, cnfequivA_in_ga(a(o(X1, X2), o(X1, X3)), X4))
CNFEQUIVA_IN_GA(o(X1, a(X2, X3)), X4) → CNFEQUIVA_IN_GA(a(o(X1, X2), o(X1, X3)), X4)
CNFEQUIVA_IN_GA(o(a(X1, X2), X3), X4) → U10_GA(X1, X2, X3, X4, cnfequivA_in_ga(a(o(X1, X3), o(X2, X3)), X4))
CNFEQUIVA_IN_GA(o(a(X1, X2), X3), X4) → CNFEQUIVA_IN_GA(a(o(X1, X3), o(X2, X3)), X4)
CNFEQUIVA_IN_GA(o(X1, X2), X3) → U11_GA(X1, X2, X3, transformB_in_ga(X1, X4))
CNFEQUIVA_IN_GA(o(X1, X2), X3) → TRANSFORMB_IN_GA(X1, X4)
TRANSFORMB_IN_GA(o(X1, X2), o(X3, X2)) → U1_GA(X1, X2, X3, transformB_in_ga(X1, X3))
TRANSFORMB_IN_GA(o(X1, X2), o(X3, X2)) → TRANSFORMB_IN_GA(X1, X3)
TRANSFORMB_IN_GA(o(X1, X2), o(X1, X3)) → U2_GA(X1, X2, X3, transformB_in_ga(X2, X3))
TRANSFORMB_IN_GA(o(X1, X2), o(X1, X3)) → TRANSFORMB_IN_GA(X2, X3)
TRANSFORMB_IN_GA(a(X1, X2), a(X3, X2)) → U3_GA(X1, X2, X3, transformB_in_ga(X1, X3))
TRANSFORMB_IN_GA(a(X1, X2), a(X3, X2)) → TRANSFORMB_IN_GA(X1, X3)
TRANSFORMB_IN_GA(a(X1, X2), a(X1, X3)) → U4_GA(X1, X2, X3, transformB_in_ga(X2, X3))
TRANSFORMB_IN_GA(a(X1, X2), a(X1, X3)) → TRANSFORMB_IN_GA(X2, X3)
TRANSFORMB_IN_GA(n(X1), n(X2)) → U5_GA(X1, X2, transformB_in_ga(X1, X2))
TRANSFORMB_IN_GA(n(X1), n(X2)) → TRANSFORMB_IN_GA(X1, X2)
CNFEQUIVA_IN_GA(o(X1, X2), X3) → U12_GA(X1, X2, X3, transformcB_in_ga(X1, X4))
U12_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → U13_GA(X1, X2, X3, cnfequivA_in_ga(o(X4, X2), X3))
U12_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(o(X4, X2), X3)
CNFEQUIVA_IN_GA(o(X1, X2), X3) → U14_GA(X1, X2, X3, transformB_in_ga(X2, X4))
CNFEQUIVA_IN_GA(o(X1, X2), X3) → TRANSFORMB_IN_GA(X2, X4)
CNFEQUIVA_IN_GA(o(X1, X2), X3) → U15_GA(X1, X2, X3, transformcB_in_ga(X2, X4))
U15_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → U16_GA(X1, X2, X3, cnfequivA_in_ga(o(X1, X4), X3))
U15_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(o(X1, X4), X3)
CNFEQUIVA_IN_GA(a(X1, X2), X3) → U17_GA(X1, X2, X3, transformB_in_ga(X1, X4))
CNFEQUIVA_IN_GA(a(X1, X2), X3) → TRANSFORMB_IN_GA(X1, X4)
CNFEQUIVA_IN_GA(a(X1, X2), X3) → U18_GA(X1, X2, X3, transformcB_in_ga(X1, X4))
U18_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → U19_GA(X1, X2, X3, cnfequivA_in_ga(a(X4, X2), X3))
U18_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(a(X4, X2), X3)
CNFEQUIVA_IN_GA(a(X1, X2), X3) → U20_GA(X1, X2, X3, transformB_in_ga(X2, X4))
CNFEQUIVA_IN_GA(a(X1, X2), X3) → TRANSFORMB_IN_GA(X2, X4)
CNFEQUIVA_IN_GA(a(X1, X2), X3) → U21_GA(X1, X2, X3, transformcB_in_ga(X2, X4))
U21_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → U22_GA(X1, X2, X3, cnfequivA_in_ga(a(X1, X4), X3))
U21_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(a(X1, X4), X3)
CNFEQUIVA_IN_GA(n(X1), X2) → U23_GA(X1, X2, transformB_in_ga(X1, X3))
CNFEQUIVA_IN_GA(n(X1), X2) → TRANSFORMB_IN_GA(X1, X3)
CNFEQUIVA_IN_GA(n(X1), X2) → U24_GA(X1, X2, transformcB_in_ga(X1, X3))
U24_GA(X1, X2, transformcB_out_ga(X1, X3)) → U25_GA(X1, X2, cnfequivA_in_ga(n(X3), X2))
U24_GA(X1, X2, transformcB_out_ga(X1, X3)) → CNFEQUIVA_IN_GA(n(X3), X2)

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1)), X1) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2)), o(n(X1), n(X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2)), a(n(X1), n(X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3))) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2), o(X3, X2)) → U42_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(o(X1, X2), o(X1, X3)) → U43_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(a(X1, X2), a(X3, X2)) → U44_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(a(X1, X2), a(X1, X3)) → U45_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(n(X1), n(X2)) → U46_ga(X1, X2, transformcB_in_ga(X1, X2))
U46_ga(X1, X2, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The argument filtering Pi contains the following mapping:
cnfequivA_in_ga(x1, x2)  =  cnfequivA_in_ga(x1)
n(x1)  =  n(x1)
a(x1, x2)  =  a(x1, x2)
o(x1, x2)  =  o(x1, x2)
transformB_in_ga(x1, x2)  =  transformB_in_ga(x1)
transformcB_in_ga(x1, x2)  =  transformcB_in_ga(x1)
transformcB_out_ga(x1, x2)  =  transformcB_out_ga(x1, x2)
U42_ga(x1, x2, x3, x4)  =  U42_ga(x1, x2, x4)
U43_ga(x1, x2, x3, x4)  =  U43_ga(x1, x2, x4)
U44_ga(x1, x2, x3, x4)  =  U44_ga(x1, x2, x4)
U45_ga(x1, x2, x3, x4)  =  U45_ga(x1, x2, x4)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
CNFEQUIVA_IN_GA(x1, x2)  =  CNFEQUIVA_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x2, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
TRANSFORMB_IN_GA(x1, x2)  =  TRANSFORMB_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x2, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x2, x4)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x2, x4)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x2, x4)
U17_GA(x1, x2, x3, x4)  =  U17_GA(x1, x2, x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x2, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x2, x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x2, x4)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x1, x2, x4)
U22_GA(x1, x2, x3, x4)  =  U22_GA(x1, x2, x4)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)
U25_GA(x1, x2, x3)  =  U25_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 29 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TRANSFORMB_IN_GA(o(X1, X2), o(X1, X3)) → TRANSFORMB_IN_GA(X2, X3)
TRANSFORMB_IN_GA(o(X1, X2), o(X3, X2)) → TRANSFORMB_IN_GA(X1, X3)
TRANSFORMB_IN_GA(a(X1, X2), a(X3, X2)) → TRANSFORMB_IN_GA(X1, X3)
TRANSFORMB_IN_GA(a(X1, X2), a(X1, X3)) → TRANSFORMB_IN_GA(X2, X3)
TRANSFORMB_IN_GA(n(X1), n(X2)) → TRANSFORMB_IN_GA(X1, X2)

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1)), X1) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2)), o(n(X1), n(X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2)), a(n(X1), n(X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3))) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2), o(X3, X2)) → U42_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(o(X1, X2), o(X1, X3)) → U43_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(a(X1, X2), a(X3, X2)) → U44_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(a(X1, X2), a(X1, X3)) → U45_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(n(X1), n(X2)) → U46_ga(X1, X2, transformcB_in_ga(X1, X2))
U46_ga(X1, X2, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The argument filtering Pi contains the following mapping:
n(x1)  =  n(x1)
a(x1, x2)  =  a(x1, x2)
o(x1, x2)  =  o(x1, x2)
transformcB_in_ga(x1, x2)  =  transformcB_in_ga(x1)
transformcB_out_ga(x1, x2)  =  transformcB_out_ga(x1, x2)
U42_ga(x1, x2, x3, x4)  =  U42_ga(x1, x2, x4)
U43_ga(x1, x2, x3, x4)  =  U43_ga(x1, x2, x4)
U44_ga(x1, x2, x3, x4)  =  U44_ga(x1, x2, x4)
U45_ga(x1, x2, x3, x4)  =  U45_ga(x1, x2, x4)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
TRANSFORMB_IN_GA(x1, x2)  =  TRANSFORMB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TRANSFORMB_IN_GA(o(X1, X2), o(X1, X3)) → TRANSFORMB_IN_GA(X2, X3)
TRANSFORMB_IN_GA(o(X1, X2), o(X3, X2)) → TRANSFORMB_IN_GA(X1, X3)
TRANSFORMB_IN_GA(a(X1, X2), a(X3, X2)) → TRANSFORMB_IN_GA(X1, X3)
TRANSFORMB_IN_GA(a(X1, X2), a(X1, X3)) → TRANSFORMB_IN_GA(X2, X3)
TRANSFORMB_IN_GA(n(X1), n(X2)) → TRANSFORMB_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
n(x1)  =  n(x1)
a(x1, x2)  =  a(x1, x2)
o(x1, x2)  =  o(x1, x2)
TRANSFORMB_IN_GA(x1, x2)  =  TRANSFORMB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TRANSFORMB_IN_GA(o(X1, X2)) → TRANSFORMB_IN_GA(X2)
TRANSFORMB_IN_GA(o(X1, X2)) → TRANSFORMB_IN_GA(X1)
TRANSFORMB_IN_GA(a(X1, X2)) → TRANSFORMB_IN_GA(X1)
TRANSFORMB_IN_GA(a(X1, X2)) → TRANSFORMB_IN_GA(X2)
TRANSFORMB_IN_GA(n(X1)) → TRANSFORMB_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • TRANSFORMB_IN_GA(o(X1, X2)) → TRANSFORMB_IN_GA(X2)
    The graph contains the following edges 1 > 1

  • TRANSFORMB_IN_GA(o(X1, X2)) → TRANSFORMB_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • TRANSFORMB_IN_GA(a(X1, X2)) → TRANSFORMB_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • TRANSFORMB_IN_GA(a(X1, X2)) → TRANSFORMB_IN_GA(X2)
    The graph contains the following edges 1 > 1

  • TRANSFORMB_IN_GA(n(X1)) → TRANSFORMB_IN_GA(X1)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(a(X1, X2), X3) → U18_GA(X1, X2, X3, transformcB_in_ga(X1, X4))
U18_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(a(X4, X2), X3)
CNFEQUIVA_IN_GA(a(X1, X2), X3) → U21_GA(X1, X2, X3, transformcB_in_ga(X2, X4))
U21_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(a(X1, X4), X3)

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1)), X1) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2)), o(n(X1), n(X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2)), a(n(X1), n(X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3))) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2), o(X3, X2)) → U42_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(o(X1, X2), o(X1, X3)) → U43_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(a(X1, X2), a(X3, X2)) → U44_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(a(X1, X2), a(X1, X3)) → U45_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(n(X1), n(X2)) → U46_ga(X1, X2, transformcB_in_ga(X1, X2))
U46_ga(X1, X2, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The argument filtering Pi contains the following mapping:
n(x1)  =  n(x1)
a(x1, x2)  =  a(x1, x2)
o(x1, x2)  =  o(x1, x2)
transformcB_in_ga(x1, x2)  =  transformcB_in_ga(x1)
transformcB_out_ga(x1, x2)  =  transformcB_out_ga(x1, x2)
U42_ga(x1, x2, x3, x4)  =  U42_ga(x1, x2, x4)
U43_ga(x1, x2, x3, x4)  =  U43_ga(x1, x2, x4)
U44_ga(x1, x2, x3, x4)  =  U44_ga(x1, x2, x4)
U45_ga(x1, x2, x3, x4)  =  U45_ga(x1, x2, x4)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
CNFEQUIVA_IN_GA(x1, x2)  =  CNFEQUIVA_IN_GA(x1)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x2, x4)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(15) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(a(X1, X2)) → U18_GA(X1, X2, transformcB_in_ga(X1))
U18_GA(X1, X2, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(a(X4, X2))
CNFEQUIVA_IN_GA(a(X1, X2)) → U21_GA(X1, X2, transformcB_in_ga(X2))
U21_GA(X1, X2, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(a(X1, X4))

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The set Q consists of the following terms:

transformcB_in_ga(x0)
U46_ga(x0, x1)
U45_ga(x0, x1, x2)
U44_ga(x0, x1, x2)
U43_ga(x0, x1, x2)
U42_ga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U18_GA(X1, X2, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(a(X4, X2))
U21_GA(X1, X2, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(a(X1, X4))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CNFEQUIVA_IN_GA(x1)  =  x1
a(x1, x2)  =  a(x1, x2)
U18_GA(x1, x2, x3)  =  U18_GA(x2, x3)
transformcB_in_ga(x1)  =  x1
transformcB_out_ga(x1, x2)  =  transformcB_out_ga(x2)
U21_GA(x1, x2, x3)  =  U21_GA(x1, x3)
n(x1)  =  n(x1)
o(x1, x2)  =  o(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x2, x3)
U43_ga(x1, x2, x3)  =  U43_ga(x1, x3)
U44_ga(x1, x2, x3)  =  U44_ga(x2, x3)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2)  =  U46_ga(x2)

Recursive path order with status [RPO].
Quasi-Precedence:
[n1, U46ga1] > [o2, U42ga2, U43ga2] > [a2, U18GA2, U21GA2, U44ga2, U45ga2] > transformcBoutga1

Status:
a2: multiset
U18GA2: multiset
transformcBoutga1: multiset
U21GA2: multiset
n1: multiset
o2: [2,1]
U42ga2: [1,2]
U43ga2: [2,1]
U44ga2: multiset
U45ga2: multiset
U46ga1: multiset


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(a(X1, X2)) → U18_GA(X1, X2, transformcB_in_ga(X1))
CNFEQUIVA_IN_GA(a(X1, X2)) → U21_GA(X1, X2, transformcB_in_ga(X2))

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The set Q consists of the following terms:

transformcB_in_ga(x0)
U46_ga(x0, x1)
U45_ga(x0, x1, x2)
U44_ga(x0, x1, x2)
U43_ga(x0, x1, x2)
U42_ga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(19) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(20) TRUE

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(o(X1, X2), X3) → U12_GA(X1, X2, X3, transformcB_in_ga(X1, X4))
U12_GA(X1, X2, X3, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(o(X4, X2), X3)
CNFEQUIVA_IN_GA(o(X1, X2), X3) → U15_GA(X1, X2, X3, transformcB_in_ga(X2, X4))
U15_GA(X1, X2, X3, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(o(X1, X4), X3)

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1)), X1) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2)), o(n(X1), n(X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2)), a(n(X1), n(X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3))) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2), o(X3, X2)) → U42_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(o(X1, X2), o(X1, X3)) → U43_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(a(X1, X2), a(X3, X2)) → U44_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(a(X1, X2), a(X1, X3)) → U45_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(n(X1), n(X2)) → U46_ga(X1, X2, transformcB_in_ga(X1, X2))
U46_ga(X1, X2, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The argument filtering Pi contains the following mapping:
n(x1)  =  n(x1)
a(x1, x2)  =  a(x1, x2)
o(x1, x2)  =  o(x1, x2)
transformcB_in_ga(x1, x2)  =  transformcB_in_ga(x1)
transformcB_out_ga(x1, x2)  =  transformcB_out_ga(x1, x2)
U42_ga(x1, x2, x3, x4)  =  U42_ga(x1, x2, x4)
U43_ga(x1, x2, x3, x4)  =  U43_ga(x1, x2, x4)
U44_ga(x1, x2, x3, x4)  =  U44_ga(x1, x2, x4)
U45_ga(x1, x2, x3, x4)  =  U45_ga(x1, x2, x4)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
CNFEQUIVA_IN_GA(x1, x2)  =  CNFEQUIVA_IN_GA(x1)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x2, x4)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(22) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(o(X1, X2)) → U12_GA(X1, X2, transformcB_in_ga(X1))
U12_GA(X1, X2, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(o(X4, X2))
CNFEQUIVA_IN_GA(o(X1, X2)) → U15_GA(X1, X2, transformcB_in_ga(X2))
U15_GA(X1, X2, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(o(X1, X4))

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The set Q consists of the following terms:

transformcB_in_ga(x0)
U46_ga(x0, x1)
U45_ga(x0, x1, x2)
U44_ga(x0, x1, x2)
U43_ga(x0, x1, x2)
U42_ga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(24) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


CNFEQUIVA_IN_GA(o(X1, X2)) → U12_GA(X1, X2, transformcB_in_ga(X1))
U12_GA(X1, X2, transformcB_out_ga(X1, X4)) → CNFEQUIVA_IN_GA(o(X4, X2))
CNFEQUIVA_IN_GA(o(X1, X2)) → U15_GA(X1, X2, transformcB_in_ga(X2))
U15_GA(X1, X2, transformcB_out_ga(X2, X4)) → CNFEQUIVA_IN_GA(o(X1, X4))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CNFEQUIVA_IN_GA(x1)  =  CNFEQUIVA_IN_GA(x1)
o(x1, x2)  =  o(x1, x2)
U12_GA(x1, x2, x3)  =  U12_GA(x2, x3)
transformcB_in_ga(x1)  =  x1
transformcB_out_ga(x1, x2)  =  transformcB_out_ga(x2)
U15_GA(x1, x2, x3)  =  U15_GA(x1, x3)
n(x1)  =  n(x1)
a(x1, x2)  =  a(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x2, x3)
U43_ga(x1, x2, x3)  =  U43_ga(x1, x3)
U44_ga(x1, x2, x3)  =  U44_ga(x2, x3)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2)  =  U46_ga(x2)

Recursive path order with status [RPO].
Quasi-Precedence:
[n1, U46ga1] > [o2, U12GA2, U15GA2, U42ga2, U43ga2] > CNFEQUIVAINGA1 > transformcBoutga1
[n1, U46ga1] > [o2, U12GA2, U15GA2, U42ga2, U43ga2] > [a2, U44ga2, U45ga2] > transformcBoutga1

Status:
CNFEQUIVAINGA1: multiset
o2: [2,1]
U12GA2: [1,2]
transformcBoutga1: multiset
U15GA2: [2,1]
n1: multiset
a2: multiset
U42ga2: [1,2]
U43ga2: [2,1]
U44ga2: multiset
U45ga2: multiset
U46ga1: multiset


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))

(25) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The set Q consists of the following terms:

transformcB_in_ga(x0)
U46_ga(x0, x1)
U45_ga(x0, x1, x2)
U44_ga(x0, x1, x2)
U43_ga(x0, x1, x2)
U42_ga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(26) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(n(X1), X2) → U24_GA(X1, X2, transformcB_in_ga(X1, X3))
U24_GA(X1, X2, transformcB_out_ga(X1, X3)) → CNFEQUIVA_IN_GA(n(X3), X2)
CNFEQUIVA_IN_GA(n(n(X1)), X2) → CNFEQUIVA_IN_GA(X1, X2)

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1)), X1) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2)), o(n(X1), n(X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2)), a(n(X1), n(X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3))) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2), o(X3, X2)) → U42_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(o(X1, X2), o(X1, X3)) → U43_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(a(X1, X2), a(X3, X2)) → U44_ga(X1, X2, X3, transformcB_in_ga(X1, X3))
transformcB_in_ga(a(X1, X2), a(X1, X3)) → U45_ga(X1, X2, X3, transformcB_in_ga(X2, X3))
transformcB_in_ga(n(X1), n(X2)) → U46_ga(X1, X2, transformcB_in_ga(X1, X2))
U46_ga(X1, X2, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, X3, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, X3, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The argument filtering Pi contains the following mapping:
n(x1)  =  n(x1)
a(x1, x2)  =  a(x1, x2)
o(x1, x2)  =  o(x1, x2)
transformcB_in_ga(x1, x2)  =  transformcB_in_ga(x1)
transformcB_out_ga(x1, x2)  =  transformcB_out_ga(x1, x2)
U42_ga(x1, x2, x3, x4)  =  U42_ga(x1, x2, x4)
U43_ga(x1, x2, x3, x4)  =  U43_ga(x1, x2, x4)
U44_ga(x1, x2, x3, x4)  =  U44_ga(x1, x2, x4)
U45_ga(x1, x2, x3, x4)  =  U45_ga(x1, x2, x4)
U46_ga(x1, x2, x3)  =  U46_ga(x1, x3)
CNFEQUIVA_IN_GA(x1, x2)  =  CNFEQUIVA_IN_GA(x1)
U24_GA(x1, x2, x3)  =  U24_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

(29) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(n(X1)) → U24_GA(X1, transformcB_in_ga(X1))
U24_GA(X1, transformcB_out_ga(X1, X3)) → CNFEQUIVA_IN_GA(n(X3))
CNFEQUIVA_IN_GA(n(n(X1))) → CNFEQUIVA_IN_GA(X1)

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The set Q consists of the following terms:

transformcB_in_ga(x0)
U46_ga(x0, x1)
U45_ga(x0, x1, x2)
U44_ga(x0, x1, x2)
U43_ga(x0, x1, x2)
U42_ga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(31) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


CNFEQUIVA_IN_GA(n(n(X1))) → CNFEQUIVA_IN_GA(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(CNFEQUIVA_IN_GA(x1)) = x1   
POL(U24_GA(x1, x2)) = 1 + x2   
POL(U42_ga(x1, x2, x3)) = 0   
POL(U43_ga(x1, x2, x3)) = 0   
POL(U44_ga(x1, x2, x3)) = 0   
POL(U45_ga(x1, x2, x3)) = 0   
POL(U46_ga(x1, x2)) = 1 + x2   
POL(a(x1, x2)) = 0   
POL(n(x1)) = 1 + x1   
POL(o(x1, x2)) = 0   
POL(transformcB_in_ga(x1)) = x1   
POL(transformcB_out_ga(x1, x2)) = x2   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CNFEQUIVA_IN_GA(n(X1)) → U24_GA(X1, transformcB_in_ga(X1))
U24_GA(X1, transformcB_out_ga(X1, X3)) → CNFEQUIVA_IN_GA(n(X3))

The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The set Q consists of the following terms:

transformcB_in_ga(x0)
U46_ga(x0, x1)
U45_ga(x0, x1, x2)
U44_ga(x0, x1, x2)
U43_ga(x0, x1, x2)
U42_ga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(33) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


CNFEQUIVA_IN_GA(n(X1)) → U24_GA(X1, transformcB_in_ga(X1))
U24_GA(X1, transformcB_out_ga(X1, X3)) → CNFEQUIVA_IN_GA(n(X3))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CNFEQUIVA_IN_GA(x1)  =  CNFEQUIVA_IN_GA(x1)
n(x1)  =  n(x1)
U24_GA(x1, x2)  =  U24_GA(x2)
transformcB_in_ga(x1)  =  x1
transformcB_out_ga(x1, x2)  =  transformcB_out_ga(x2)
a(x1, x2)  =  a(x1, x2)
o(x1, x2)  =  o(x1, x2)
U42_ga(x1, x2, x3)  =  U42_ga(x2, x3)
U43_ga(x1, x2, x3)  =  U43_ga(x1, x3)
U44_ga(x1, x2, x3)  =  U44_ga(x2, x3)
U45_ga(x1, x2, x3)  =  U45_ga(x1, x3)
U46_ga(x1, x2)  =  U46_ga(x2)

Recursive path order with status [RPO].
Quasi-Precedence:
[n1, U24GA1, U46ga1] > [o2, U42ga2, U43ga2] > [a2, U44ga2, U45ga2] > [CNFEQUIVAINGA1, transformcBoutga1]

Status:
CNFEQUIVAINGA1: multiset
n1: multiset
U24GA1: multiset
transformcBoutga1: multiset
a2: [1,2]
o2: multiset
U42ga2: multiset
U43ga2: multiset
U44ga2: [2,1]
U45ga2: [1,2]
U46ga1: multiset


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))

(34) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

transformcB_in_ga(n(n(X1))) → transformcB_out_ga(n(n(X1)), X1)
transformcB_in_ga(n(a(X1, X2))) → transformcB_out_ga(n(a(X1, X2)), o(n(X1), n(X2)))
transformcB_in_ga(n(o(X1, X2))) → transformcB_out_ga(n(o(X1, X2)), a(n(X1), n(X2)))
transformcB_in_ga(o(X1, a(X2, X3))) → transformcB_out_ga(o(X1, a(X2, X3)), a(o(X1, X2), o(X1, X3)))
transformcB_in_ga(o(a(X1, X2), X3)) → transformcB_out_ga(o(a(X1, X2), X3), a(o(X1, X3), o(X2, X3)))
transformcB_in_ga(o(X1, X2)) → U42_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(o(X1, X2)) → U43_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(a(X1, X2)) → U44_ga(X1, X2, transformcB_in_ga(X1))
transformcB_in_ga(a(X1, X2)) → U45_ga(X1, X2, transformcB_in_ga(X2))
transformcB_in_ga(n(X1)) → U46_ga(X1, transformcB_in_ga(X1))
U46_ga(X1, transformcB_out_ga(X1, X2)) → transformcB_out_ga(n(X1), n(X2))
U45_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(a(X1, X2), a(X1, X3))
U44_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(a(X1, X2), a(X3, X2))
U43_ga(X1, X2, transformcB_out_ga(X2, X3)) → transformcB_out_ga(o(X1, X2), o(X1, X3))
U42_ga(X1, X2, transformcB_out_ga(X1, X3)) → transformcB_out_ga(o(X1, X2), o(X3, X2))

The set Q consists of the following terms:

transformcB_in_ga(x0)
U46_ga(x0, x1)
U45_ga(x0, x1, x2)
U44_ga(x0, x1, x2)
U43_ga(x0, x1, x2)
U42_ga(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(35) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(36) YES